PR summary 044631201f

Import changes for modified files

No significant changes to the import graph

Declarations diff

+ instance : Quiver (Arrow T)

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

./scripts/reporting/technical-debt-metrics.sh pr_summary

!bench

Benchmark results for 6b12b77 against 0446312 are in. No significant results found. @JovanGerb

• 🟥 build//instructions: +17.0G (+0.01%)

Small changes (1✅)

• ✅ build/module/Mathlib.Tactic.FunProp.Decl//instructions: -293.6M (-4.72%)

I think the performance impact is neutral.

I'm sure this is the correct thing to do, but can you explain a bit what the issue was? And why doesn't

instance : Category (Arrow T) where
  Hom := Arrow.Hom
  __ := inferInstanceAs <| Category (Comma (𝟭 T) (𝟭 T))

work?

The issue is in the data fields id and comp. In the old version, these had types corresponding to Comma (𝟭 T) (𝟭 T). inferInstanceAs packages the data so that the definition doesn't leak through.

The option you suggested doesn't compile. It is possible to write

instance : Category (Arrow T) where
  Hom := Arrow.Hom
  __ : Category (Arrow T) := inferInstanceAs <| Category (Comma (𝟭 T) (𝟭 T))

And this does give the right defeq. But the generated term is a lot more unnecessarily complicated. #print instCategoryArrow gives

  let __spread.0 :=
    { Hom := instCategoryArrow._aux_1, id := instCategoryArrow._aux_3, comp := @instCategoryArrow._aux_5 T inst,
      id_comp := ⋯, comp_id := ⋯, assoc := ⋯ };
  { Hom := Arrow.Hom, id := 𝟙, comp := @CategoryStruct.comp (Arrow T) __spread.0.toCategoryStruct, id_comp := ⋯,
    comp_id := ⋯, assoc := ⋯ }

Thanks!

maintainer merge

🚀 Pull request has been placed on the maintainer queue by robin-carlier.

I would trust your judgement here!

bors merge

Pull request successfully merged into master.

Build succeeded:

• ci (staging) / Post-CI job
• ci (staging) / Lint style
• ci (staging) / Post-Build Step
• ci (staging) / Build